T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:es-E(es).
es-dtype(es; loc(e); x; T)
 (e':es-E(es). 
 es-locl(es; e'; e)
  ((es-after(es; x; e') = es-when(es; x; e')  T))
  es-le(es; e'; (last change to x before e))) 

latex

Definitions	guard(T), P  Q, es-le(es; e; e'), A c B, x:A. B(x), e<e'.P(e), es-locl(es; e; e'), P  Q, P  Q, P  Q, prop{i:l}, t  T, P  Q, EqDecider(T), x:A. B(x), e(e1,e2].P(e), e[e1,e2).P(e), decidable(P), es-dtype(es; i; x; T)
Lemmas	last-change-property, es-locl transitivity1, last-change-after-property, es-locl-iff, es-loc-pred, loc-last-change, es-le-not-locl, last-change-equal, es-le weakening, last-change wf, decidable es-locl, es-causl wf, assert-changed, assert wf, iff wf, bool wf, event system wf, Id wf, es-loc wf, es-dtype wf, es-E wf, es-locl wf, es-when wf, es-vartype wf, es-after wf, not wf